AXIOM EVSUM
(∀ X) (∀ Y) (XεI∧YεI⊃X+Y=EVAL LIST('PLUS,X,Y)) 

PROOF ONE 

1:	'17εI∧'34εI⊃'17+'34=EVAL LIST('PLUS,'17,'34) BY AXIOM(EVSUM
,'17,'34) 

2:	17='17 BY INTQUOTE 17 

3:	34='34 BY INTQUOTE 34 

4:	17εI BY ISINT 17 

5:	34εI BY ISINT 34 

6:	'17εI BY REPL(4,2,1) 

7:	'34εI BY REPL(5,3,1) 

8:	'17εI∧'34εI BY AI(6,7) 

9:	'17+'34=EVAL LIST('PLUS,'17,'34) BY MP(8,1) 

10:	LIST('PLUS,'17,'34)='(PLUS 17 34) BY EVLIST('PLUS,'17,'34) 

11:	'17+'34=EVAL '(PLUS 17 34) BY REPL(9,10,1) 

12:	EVAL '(PLUS 17 34)='51 BY EVEVAL (17+34) 

13:	'17+'34='51 BY REPL(11,12,1) 

14:	'17+34='51 BY REPR(13,3,1) 

15:	17+34='51 BY REPR(14,2,1) 

16:	51='51 BY INTQUOTE 51 

17:	17+34=51 BY REPR(15,16,1)